(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v3 () Bool)
(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(declare-fun v6 () Bool)
(declare-fun v7 () Bool)
(declare-fun v8 () Bool)
(declare-fun i1 () Int)
(declare-fun str0 () String)
(declare-fun str1 () String)
(declare-fun str2 () String)
(declare-fun str3 () String)
(declare-fun str4 () String)
(declare-fun v15 () Bool)
(declare-fun v27 () Bool)
(assert (= (> i1 56 (abs 51)) v1 (distinct v8 v4) v3 v0))
(assert (or v27 v0 (str.prefixof str1 (str.++ str3 "UXkQw9ozyOxX5")) (<= 308 (str.len str0)) (str.prefixof str1 (str.++ str3 "UXkQw9ozyOxX5")) (= i1 56 56 51)))
(push)
(pop)
(assert (distinct (str.len str2) 308))
(assert (and (<= 55 i1 749) (> i1 56 (abs 51)) v15 (<= 51 (abs 51) (str.len str3) 749 (str.len str2)) v3 (= (str.replace_re str4 re.allchar str3) (str.++ str3 "UXkQw9ozyOxX5") (str.++ str3 "UXkQw9ozyOxX5"))))
(assert (<= 51 (abs 51) (str.len str3) 749 (str.len str2)))
(assert (str.in_re str1 re.allchar))
(assert (xor v4 (or (str.in_re (str.++ str1 str0 (str.from_int (str.to_int str4)) (str.++ str3 "UXkQw9ozyOxX5") "n") re.allchar) v1 v15)))
(push)
(check-sat)
